@string{acta = "Acta Inf."}
@string{JACM = "J. ACM"}
@string{cacm = "Commun. ACM"}
@string{charme = "CHARME"}
@string{jalg = "J. Alg."}
@string{asian = "Proc. Asian Comp. Sci. Conf."}
@string{cav = "Computer Aided Verif."}
@string{cc = "Comp. Construct."}
@string{concur = "Proc.\ {CONCUR}"}
@string{entcs = "Elec. Notes in Theor. Comp. Sci."}
@string{esop = "European Symp. On Programming"}
@string{fmsd = "Formal Methods in System Design"}
@string{fse = "Found. of Softw. Eng."}
@string{icalp = "Int. Colloq. on Automata, Langs., and Programming"}
@string{ipl = "Inf. Proc. Let."}
@string{kap = "Kluwer Acad."}
@string{lics = "Logic in Comp. Sci."}
@string{lncs = "Lec. Notes in Comp. Sci."}
@string{loplas = "Let. on Prog. Lang. and Syst."}
@string{paste = "Prog. Analysis for Softw. Tools and Eng."}
@string{pldi = "Prog. Lang. Design and Impl."}
@string{popl = "Princ. of Prog. Lang."}
@string{sas = "Static Analysis Symp."}
@string{socc = "Comp. Construct."}
@string{spin = "Spin Workshop"}
@string{spv = "Springer-Verlag"}
@string{tacas = "Tools and Algs.\ for the Construct.\ and Anal.\ of Syst."}
@string{tacs = "Theor.\ Aspects of Computer Software"}
@string{tcs = "Theor. Comp. Sci."}
@string{toplas = "Trans. on Prog. Lang. and Syst."}
@string{tosem = "Trans. on Softw. Eng. and Method."}
@string{tse = "Trans. on Softw. Eng."}
@string{vmcai = "Verif., Model Checking, and Abs.\ Interp."}

@inproceedings{CONCUR:BEM97,
  author   = "A. Bouajjani and J. Esparza and O. Maler",
  title    = "Reachability Analysis of Pushdown Automata: {A}pplication to Model Checking",
  booktitle = concur,
  year = 1997
}

@inproceedings {POPL:AG00,
  author    = "R. Alur and R. Grosu",
  title     = "Modular Refinement of Hierarchic State Machines",
  booktitle = popl,
  pages     = "390--402",
  month     = jan,
  year      = 2000
}

@inproceedings{ICALP:AKY99,
  author    = "R. Alur and S. Kannan and M. Yannakakis",
  title     = "Communicating Hierarchical State Machines",
  booktitle = icalp,
  publisher = spv,
  series    = lncs,
  volume    = 1644,
  year      = 1999,
  pages     = "169--178"
}

@inproceedings{CONCUR:BS92,
  author    = "O. Burkart and B. Steffen",
  title     = "Model Checking for Context-Free Processes",
  booktitle = concur,
  pages     = "123--137",
  publisher = spv,
  series    = lncs,
  volume    = 630,
  year      = 1992
}

@inproceedings{CONCUR:BS94,
  author  = "O. Burkart and B. Steffen",
  title   = "Pushdown Processes: Parallel Composition and Model Checking",
  booktitle = concur,
  series    = lncs,
  volume    = 836,
  year      = 1994
}

@inproceedings{ICALP:BS97,
  author    = "O. Burkart and B. Steffen",
  title     = "Model Checking the Full Modal Mu-Calculus for Infinite Sequential Processes",
  booktitle = icalp,
  series    = lncs,
  volume    = "1256",
  pages     = "419--429",
  year      = 1997
}

@inproceedings{GTCCS:CM90,
  author    = "B. Caucal and R. Monfort",
  title     = "On the Transition Graphs of Automata and Grammars",
  booktitle = "Graph Theoretic Concepts in Computer Science",
  series    = lncs,
  volume    = "484",
  pages     = "311--337",
  year      = 1990
}

@inbook{HTCSB:E90,
  author    = "E.A. Emerson",
  title     = "Temporal and Modal Logic",
  booktitle = "Handbook of Theoretical Computer Science, Volume B",
  editor    = "J. van Leeuwen",
  year      = 1990,
  publisher = "The M.I.T. Press/Elsevier"
}

@article{ENTCS:fww97,
  author  = "A. Finkel and B.Willems and P. Wolper",
  title   = "A Direct Symbolic Approach to Model Checking Pushdown Systems",
  journal = entcs,
  volume  = "9",
  year    = 1997
}

@inproceedings{CAV:W96,
  author    = "I. Walukiewicz",
  title     = "Pushdown Processes: {G}ames and Model-Checking",
  booktitle = cav,
  series    = lncs,
  pages     = "62--74",
  month     = aug,
  year      = 1996
}

@inproceedings{SAS:MSS99,
  author = "M. M{\"{u}}ller-Olm and D. Schmidt and B. Steffen",
  title = "Model-Checking: {A} Tutorial Introduction",
  booktitle = sas,
  month = sep,
  pages = "330--354",
  publisher = spv,
  series = lncs,
  volume = 1694,
  year = 1999
}

@inproceedings{ASIAN:K99,
  author = "J. Knoop",
  title = "Demand-driven Model Checking for Context-Free Processes",
  booktitle = asian,
  editor = "P.S. Thiagarajan and R. Yap",
  month = dec,
  pages = "201--213",
  publisher = spv,
  series = lncs,
  volume = 1742,
  year = 1999,
}

@Unpublished{Knoop00-PC-TWR,
  author  = "J. Knoop",
  title   = "Personal Communication to {Thomas Reps}",
  year    = 2000,
  Month   = aug
}

@inproceedings{CAV:CS91,
  author = "R. Cleaveland and B. Steffen",
  title = "A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus",
  booktitle = cav,
  pages = "48--58",
  publisher = spv,
  series = lncs,
  volume = 575,
  year = 1992
}

@inproceedings{CAV:CKS92,
  author = "R. Cleaveland and M. Klein and B. Steffen",
  title = "Faster Model Checking in the Modal Mu-Calculus",
  booktitle = cav,
  editor = "G.v. Bochmann and D.K. Probst",
  pages = "410--422",
  publisher = spv,
  series = lncs,
  volume = 663,
  year = 1992
}

@Book{book:McM93,
  Title     = "Symbolic Model Checking",
  Author    = "K.L. McMillan",
  Year      = 1993,
  Publisher = kap
}

@Unpublished{Clarke97-PC-TWR,
  author= "Clarke, Jr., E.M.",
  title="Personal Communication to {T. Reps}",
  year=1997,
  Month=nov
}
@inproceedings{CAV:CVWY90,
  author    = "C. Courcoubetis and M. Vardi and P. Wolper and M.Yannakakis",
  title     = "Memory efficient algorithms for the verification of temporal properties",
  booktitle = cav,
  publisher = spv,
  series    = lncs,
  volume    = 531,
  pages     = "233--242",
  year      = 1990
}

@inproceedings{SPIN:HPY96,
  author    = "G.J. Holzmann and D. Peled and M. Yannakakis",
  title     = "On Nested Depth First Search",
  booktitle = spin,
  pages     = "23--32"
}

@TECHREPORT{UWCS:TR1424,
  AUTHOR =        "E. Yahav and T. Reps and M. Sagiv",
  TITLE =         "{LTL} Model Checking for Systems with Unbounded Number of Dynamically Created Threads and Objects",
  INSTITUTION =   "Comp. Sci. Dept., Univ. of Wisconsin",
  ADDRESS =       "Madison, WI",
  TYPE =          "Tech. Rep.",
  NUMBER =        "TR-1424",
  MONTH =         mar,
  YEAR =          2001,
}

@TECHREPORT{UWCS:TR1425,
  AUTHOR =        "M. Benedikt and P. Godefroid and T. Reps",
  TITLE =         "Model Checking of Unrestricted Hierarchical State Machines (Extended Abstract).",
  INSTITUTION =   "Comp. Sci. Dept., Univ. of Wisconsin",
  ADDRESS =       "Madison, WI",
  TYPE =          "Tech. Rep.",
  NUMBER =        "TR-1425",
  MONTH =         mar,
  YEAR =          2001,
}

@inproceedings{CAV:DDP99,
  author    = "S. Das and D.L. Dill and S. Park",
  title     = "Experience with Predicate Abstraction",
  Editors   = "N. Halbwachs and D. Peled",
  booktitle = cav,
  month     = jul,
  publisher = spv,
  year      = 1999,
  pages     = "160--171"
}

@inproceedings{CAV:CGJLV00,
  author    = "E.M. Clarke and O. Grumberg and S. Jha and Y. Lu and H. Veith",
  title     = "Counterexample-Guided Abstraction Refinement",
  booktitle = cav,
  Month     = jul,
  Year      = 2000,
  Pages     = "154--169"
}
@inproceedings{CAV:GS97,
  Author    = "S. Graf and H. Sa{\"\i}di",
  Title     = "Construction of Abstract State Graphs with {PVS}",
  Booktitle = cav,
  Series    = lncs,
  Volume    = 1254,
  Year      = 1997,
  Pages     = "72--83"
}
@inproceedings{LNCS:CJ95,
  author = "E.M. Clarke and S. Jha",
  title = "Symmetry and Induction in Model Checking",
  booktitle = "Comp.\ Sci.\ Today: {R}ecent Trends and Developments",
  series = lncs,
  volume = 1000,
  year = 1995,
  pages = "455--470"
}
@InProceedings{POPL:Yahav01,
  author =       "E. Yahav",
  title =        "Verifying Safety Properties of Concurrent {J}ava
                 Programs using 3-valued Logic",
  Booktitle =    popl,
  Pages =        "27--40",
  Month =        jan,
  Year =         "2001"
}
@inproceedings{CAV:ES93,
  author    = "E. Emerson and A.P. Sistla",
  title     = "Symmetry and Model Checking",
  booktitle = cav,
  Month     = "June/July",
  Year      = 1993,
  Editor    = "C. Courcoubetis",
  Pages     = "463--478"
}
@InProceedings{ICALP:BGR01,
  Author    = "M. Benedikt and P. Godefroid and T. Reps",
  Title     = "Model Checking of Unrestricted Hierarchical State Machines",
  Booktitle = icalp,
  Year      = 2001,
  Pages     = "652--666"
}
@InProceedings{SPIN:BR00,
  Author    = "T. Ball and S.K. Rajamani",
  Title     = "Bebop: {A} Symbolic Model Checker for {B}oolean Programs",
  Booktitle = spin,
  Series    = lncs,
  Volume    = "1885",
  Year      = 2000,
  Pages     = "113--130"
}
@InProceedings{PASTE:BR01,
  Author    = "T. Ball and S.K. Rajamani",
  Title     = "Bebop: A Path-sensitive Interprocedural Dataflow Engine",
  Booktitle = paste,
  Month     = jun,
  Year      = 2001,
  Pages     = "97--103"
}
@InProceedings{CAV:AEY01,
  Author    = "R. Alur and K. Etessami and M. Yannakakis",
  Title     = "Analysis of Recursive State Machines",
  Booktitle = cav,
  Month     = jul,
  Year      = 2001,
  Pages     = "207--220"
}
@InProceedings{LICS:VW86,
  Author    = "M.Y. Vardi and P. Wolper",
  Title     = "An Automata-Theoretic Approach to Automatic Program Verification",
  Booktitle = lics,
  Month     = jun,
  Year      = 1986,
  Pages     = "322--331"
}

@InProceedings{CAV:EHRS00,
  Author    = "J. Esparza and D. Hansel and P. Rossmanith and S. Schwoon",
  Title     = "Efficient Algorithms for Model Checking Pushdown Systems",
  Booktitle = cav,
  Series    = lncs,
  Volume    = 1855,
  Pages     = "232--247",
  Month     = jul,
  Year      = 2000
}

@InProceedings{LICS:EL86,
  Author    = "E.A. Emerson and C. Lei",
  Title     = "Efficient Model Checking in Fragments of the Propositional Mu-Calculus",
  Booktitle = lics,
  Month     = jun,
  Year      = 1986,
  Pages     = "267--278"
}

@inproceedings{CAV:Chou99,
  author    = "C.-T. Chou",
  title     = "The Mathematical Foundation of Symbolic Trajectory Evaluation",
  Editors   = "N. Halbwachs and D. Peled",
  booktitle = cav,
  month     = jul,
  publisher = spv,
  year      = 1999
}

@Article{FMSD:SB95,
         Author = "C.-J.H. Seger and R.E. Bryant",
         Title = "Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories",
         Month = mar,
         Year = 1995,
         Journal = fmsd,
         Volume = 6,
         Number = 2,
         Pages = "147--189"
}

@PHDTHESIS{Thesis:Jain97,
        AUTHOR = "A. Jain",
        Title ="Formal Verification by Symbolic Trajectory Evaluation",
        School = "Carnegie Mellon Univ.",
        address = "Pittsburgh, PA",
        Month = jul,
        YEAR = 1997
}

@InProceedings{CONCUR:BG00,
  author =       "G. Bruns and P. Godefroid",
  title =        "Generalized Model Checking: {R}easoning about Partial State Spaces",
  booktitle =    concur,
  publisher =    spv,
  year =         "2000"
}

@InProceedings{CAV:BG99,
  author =       "G. Bruns and P. Godefroid",
  year =         "1999",
  title =        "Model Checking Partial State Spaces with 3-Valued Temporal Logics",
  booktitle =    cav,
  pages =        "274--287"
}

@InProceedings{CONCUR:GHJ10,
  author =       "P. Godefroid and M. Huth and R. Jagadeesan",
  title =        "Abstraction-Based Model Checking Using Modal Transition Systems",
  booktitle =    concur,
  publisher =    spv,
  year =         "2001",
  pages =        "426--440"
}

@InProceedings{TACAS:BPR01,
  Author    = "T. Ball and A. Podelski and S.K. Rajamani",
  Title     = "{B}oolean and {C}artesian Abstraction for Model Checking {C} Programs",
  Booktitle = tacas,
  Year      = 2001,
  Pages     = "268--283"
}

@InProceedings{CAV:BR01,
  Author    = "T. Ball and S.K. Rajamani",
  Title     = "The {SLAM} Toolkit",
  Booktitle = cav,
  Year      = 2001
}

@InProceedings{FSE:AY98,
  Author    = "R. Alur and M. Yannakakis",
  Title     = "Model Checking of Hierarchical State Machines",
  Booktitle = fse,
  Year      = 1998,
  Pages     = "175--188"
}

@InProceedings{PLDI:BMMR01,
  Author    = "T. Ball and R. Majumdar and T. Millstein and S.K. Rajamani",
  Title     = "Automatic Predicate Abstraction of {C} Programs",
  Booktitle = pldi,
  Publisher = "ACM Press",
  Address   = "New York, NY",
  Year      = 2001
}

@InProceedings{PLDI:DLS02,
  Author    = "M. Das and S. Lerner and M. Seigle",
  Title     = "{ESP}: {P}ath-Sensitive Program Verification in Polynomial Time",
  Booktitle = pldi,
  Publisher = "ACM Press",
  Address   = "New York, NY",
  Year      = 2002,
  Pages     = "57--68"
}

@Article{TOPLAS:CGL94,
    Author  = "E.M. Clarke and O. Grumberg and D.E. Long",
    Title   = "Model Checking and Abstraction",
    Journal = toplas,
    Volume  = 16,
    Number  = 5,
    Year    = 1994,
    Pages   = "1512--1542"
}

@InProceedings{CHARME:McMillan99,
  Author    = "K.L. McMillan",
  Title     = "Verification of Infinite State Systems by Compositional Model Checking",
  Booktitle = charme,
  Year      = 1999,
  Pages     = "219--234"
}

@InProceedings{TACAS:EKS01,
  author    = "J. Esparza and A. Ku{\v{c}}era and S. Schwoon",
  title	    = "Model-Checking {LTL} with Regular Valuations for Pushdown Systems",
  booktitle = tacas,
  publisher = spv,
  series    = lncs,
  volume    = 2031,
  pages	    = "316--339",
  year      = 2001
}

@TECHREPORT{Cornell:TR1851,
  AUTHOR =        "J. Ezick and D.W. Richardson and T. Teitelbaum",
  TITLE =         "Practical Model Checking and Example Generation for Context-Free Processes",
  INSTITUTION =   "Dept. of Comp. Sci., Cornell Univ",
  ADDRESS =       "Ithaca, NY",
  TYPE =          "Tech. Rep.",
  NUMBER =        "TR2001-1851",
  YEAR =          2001,
}

@inproceedings{SPIN:MT98,
  author    = "L. Millett and T. Teitelbaum",
  title     = "Slicing {P}romela and its Applications to Model Checking, Simulation, and Protocol Understanding",
  booktitle = spin,
  year = 1998
}

@InProceedings{ESOP:YRSW03,
   Author = "E. Yahav and T. Reps and M. Sagiv and R. Wilhelm", 
   Title = "Verifying Temporal Heap Properties Specified via Evolution Logic",
   Booktitle = esop,
   Year = 2003
}

@MISC{URL:Moped,
  Author = "S. Schwoon",
  Title  = "{Moped} System",
  Note   = "http://www.fmi.uni-stuttgart.de/szs/tools/moped/",
  Institution = {U. Stuttgart}
}

@misc{URL:wpds,
  title = "Weighted {PDS} Library",
  note = "http://www.fmi.uni-stuttgart.de/szs/tools/wpds/",
  institution = {U. Stuttgart}
}

@MISC{URL:SLAM,
  Title = "{SLAM} Toolkit",
  Note = "http://research.microsoft.com/slam/"
}

@PHDTHESIS{Thesis:Dams96,
        AUTHOR = "D. Dams",
        Title ="Abstract Interpretation and Partial Refinement for Model Checking",
        School = "Technical Univ. of Eindhoven",
        address = "Eindhoven, The Netherlands",
        Month = jul,
        YEAR = 1996
}

@InProceedings{CAV:CGKS02,
   Author = "E. Clarke and A. Gupta and J. Kukula and O. Strichman",
   Title = "{SAT} Based Abstraction-Refinement using {ILP} and Machine Learning Techniques",
   Booktitle = cav,
   Year = 2002
}

@InProceedings{VMCAI:DK03,
   Author = "D. Dams and K.S. Namjoshi",
   Title = "Shape Analysis through Predicate Abstraction and Model Checking",
   Booktitle = vmcai,
   Year = 2003
}

@inproceedings{POPL:BET03,
  author = "A. Bouajjani and J. Esparza and T. Touili",
  title = "A Generic Approach to the Static Analysis of Concurrent Programs with Procedures",
  booktitle = POPL,
  year = 2003,
  pages = "62--73"
} 

@PHDTHESIS{Thesis:Schwoon02,
        AUTHOR = "S. Schwoon",
        Title ="Model-Checking Pushdown Systems",
        School = "Technical Univ.\ of Munich",
        address = "Munich, Germany",
        Month = "July",
        YEAR = "2002"
}

@InProceedings{ICALP:Cachat02,
  Author    = "T. Cachat",
  Title     = "Symbolic Strategy Synthesis for Games on Pushdown Graphs",
  Booktitle = icalp,
  Year      = 2002,
  Pages     = "704--715"
}

@InProceedings{CAV:KV00,
  author    = "O. Kupferman and M.Y. Vardi",
  title     = "An Automata-Theoretic Approach to Reasoning about Infinite-State Systems",
  booktitle = cav,
  year      = 2000
}

@InProceedings{TACAS:ALTM01,
  Author    = "R. Alur and S. La Torre and P. Madhusudan",
  Title     = "Modular Strategies for Recursive Game Graphs",
  Booktitle = tacas,
  Year      = 2003,
  Pages     = "363--378"
}

@InProceedings{CAV:BRKLLMGYCT05,
  author    = "G. Balakrishnan and T. Reps and N. Kidd and A. Lal and J. Lim and D. Melski and R. Gruian and S. Yong and C.-H. Chen and T. Teitelbaum",
  title     = "Model Checking x86 Executables with {CodeSurfer/x86} and {WPDS++}",
  booktitle = cav,
  year      = 2005
}

@inproceedings{EuroSys:BBCLLMORU06,
 author = "T. Ball and E. Bounimova and B. Cook and V. Levin and J. Lichtenberg and C. McGarvey and B. Ondrusek and S.K. Rajamani and A. Ustuner",
 title = "Thorough Static Analysis of Device Drivers",
 booktitle = "EuroSys",
 year = 2006
 }

@InProceedings{TACAS:CCKRT06,
  Author    = "S. Chaki and E. Clarke and N. Kidd and T. Reps and T. Touili",
  Title     = "Verifying Concurrent Message-Passing {C} Programs with Recursive Calls",
  Booktitle = tacas,
  Year      = 2006
}

@InProceedings{PLDI:QW04,
  Author    = "S. Qadeer and D. Wu",
  Title     = "{KISS}: {K}eep it Simple and Sequential",
  Year      = 2004,
  Booktitle = pldi
}

@InProceedings{CAV:BHV04,
  Author    = "A. Bouajjani and P. Habermehl and T. Vojnar",
  Title     = "Abstract Regular Model Checking",
  Year      = 2004,
  Booktitle = cav
}

@BOOK{Book:Buechi88,
  Author    = "J.R. B{\"u}chi",
  Title     = "Finite Automata, their Algebras and Grammars",
  Note      = "D. Siefkes (ed.)",
  Publisher = spv,
  Year      = 1988
}

@Unpublished{Unpublished:CI06,
  Author = "S. Chaki and J. Ivers",
  Title  = "Low-Level Software Verification",
  Year   = 2006,
  Note   = "Unpublished manuscript"
}

@InProceedings{CAV:IG05,
  Author    = "I. Rabinovitz and O. Grumberg",
  Title     = "Bounded Model Checking of Concurrent Programs",
  Booktitle = cav,
  Year      = 2005
}

@InProceedings{TACAS:CKL04,
  Author    = "E.M. Clarke and D. Kroening and F. Lerda",
  Title     = "A Tool For Checking {ANSI--C} Programs",
  Booktitle = tacas,
  Year      = 2004
}

@InProceedings{TACAS:BCCZ99,
  Author    = "A. Biere and A. Cimatti and E.M. Clarke and Y. Zhu",
  Title     = "Symbolic Model Checking Without {BDDs}",
  Booktitle = tacas,
  Year      = 1999
}
